Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    from(X)  → cons(X,from(s(X)))
2:    2ndspos(0,Z)  → rnil
3:    2ndspos(s(N),cons(X,cons(Y,Z)))  → rcons(posrecip(Y),2ndsneg(N,Z))
4:    2ndsneg(0,Z)  → rnil
5:    2ndsneg(s(N),cons(X,cons(Y,Z)))  → rcons(negrecip(Y),2ndspos(N,Z))
6:    pi(X)  → 2ndspos(X,from(0))
7:    plus(0,Y)  → Y
8:    plus(s(X),Y)  → s(plus(X,Y))
9:    times(0,Y)  → 0
10:    times(s(X),Y)  → plus(Y,times(X,Y))
11:    square(X)  → times(X,X)
There are 9 dependency pairs:
12:    FROM(X)  → FROM(s(X))
13:    2ndspos#(s(N),cons(X,cons(Y,Z)))  → 2ndsneg#(N,Z)
14:    2ndsneg#(s(N),cons(X,cons(Y,Z)))  → 2ndspos#(N,Z)
15:    PI(X)  → 2ndspos#(X,from(0))
16:    PI(X)  → FROM(0)
17:    PLUS(s(X),Y)  → PLUS(X,Y)
18:    TIMES(s(X),Y)  → PLUS(Y,times(X,Y))
19:    TIMES(s(X),Y)  → TIMES(X,Y)
20:    SQUARE(X)  → TIMES(X,X)
The approximated dependency graph contains 4 SCCs: {13,14}, {12}, {17} and {19}.
Tyrolean Termination Tool  (0.04 seconds)   ---  May 3, 2006